package joc.nextgen.dbi;

import static joc.nextgen.JOC.unchanged;
import joc.nextgen.dbi.JOC.PostCondition;
import joc.nextgen.dbi.JOC.PreCondition;

public class TimeOfDayContract extends TimeOfDay {
	@ClassInvariant
	public void invariant() {
		assert getHour() >= 0 && getHour() <= 23;
		assert getMinute() >= 0 && getMinute() <= 59;
		assert getSecond() >= 0 && getSecond() <= 59;
	}

	@Override
	public void setHour(final int hour) {
		new PreCondition() {
			{
				assert hour >= 0 && hour <= 23;
			}
		};
		new PostCondition() {
			{
				assert getHour() == hour;
				unchanged(getMinute(), getSecond());
			}
		};
	}

	@Override
	public void setMinute(final int minute) {
		new PreCondition() {
			{
				assert minute >= 0 && minute <= 59;
			}
		};
		new PostCondition() {
			{
				assert getMinute() == minute;
				unchanged(getSecond(), getHour());
			}
		};
	}

	@Override
	public void setSecond(final int second) {
		new PreCondition() {
			{
				assert second >= 0 && second <= 59;
			}
		};
		new PostCondition() {
			{
				assert getSecond() == second;
				unchanged(getMinute(), getHour());
			}
		};
	}

}